|
|
Current transducer's characteristics
Čížek, Ondřej ; Bulín, Tomáš (referee) ; Huzlík, Rostislav (advisor)
In this bachelor thesis are described all used current transducers, the way of their function and at each of them are described their properties. After that is described program LabVIEW and measurement, which happened by using it with specialization on frequency characteristics and their evaluation.
|
|
|
Tool for Abstract Regular Model Checking
Chalk, Matěj ; Rogalewicz, Adam (referee) ; Hruška, Martin (advisor)
Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.
|
|
|
Library for Finite Automata and Transducers
Bieliková, Michaela ; Lengál, Ondřej (referee) ; Hruška, Martin (advisor)
Finite state automata are widely used in the field of computer science such as formal verification, system modelling, and natural language processing. However, the models representing the reality are complicated and can be defined upon big alphabets, or even infinite alphabets, and thus contain a lot of transitions. In these cases, using classical finite state automata is not very efficient. Symbolic automata are more concise by employing predicates as transition labels. Finite state transducers also have a wide range of application such as linguistics or formal verification. Symbolic transducers replace classic transition labels with two predicates, one for input symbols and one for output symbols. The goal of this thesis is to design a library for letter and symbolic automata and transducers which will be suitable for fast prototyping.
|
|
|
Synchronous Formal Systems Based on Grammars and Transducers
Horáček, Petr ; Janoušek, Jan (referee) ; Yamamura,, Akihito (referee) ; Meduna, Alexandr (advisor)
Tato disertační práce studuje synchronní formální systémy založené na gramatikách a převodnících a zkoumá jak jejich teoretické vlastnosti, tak i perspektivy praktických aplikací. Práce představuje nové koncepty a definice vycházející ze známých principů řízeného přepisování a synchronizace. Navrhuje alternativní způsob synchronizace bezkontextových gramatik, založený na propojení pravidel. Tento princip rozšiřuje také na řízené gramatiky, konkrétně gramatiky s rozptýleným kontextem a maticové gramatiky. Dále je představen na podobném principu založený nový druh převodníku, tzv. pravidlově omezený převodník. Jedná se o systém složený z konečného automatu a bezkontextové gramatiky. Práce prezentuje nové teoretické výsledky ohledně generativní a přijímajicí síly. Poslední část práce zkoumá možnosti lingvisticky orientovaných aplikací se zameřením na překlad přirozeného jazyka. Diskutuje a srovnává hlavní výhody nových modelů s využitím vybraných případových studií z českého, anglického a japonského jazyka pro ilustraci.
|
|
|
Transducer Systems
Skácel, Jiří ; Kučera, Jiří (referee) ; Meduna, Alexandr (advisor)
This document defines systems of pushdown transducers. The idea of cooperating distributed grammar systems for components working on one word is adjusted for use of transducers instead of grammars. The transducers cooperate by passing output of one to input of another component. It discusses their descriptive power and equivalency between systems with arbitrary numbers of components. The main conclusion is then comparison of their descriptive power with Turing machines with regard to their translation and accepted languages.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
V této práci se zabýváme regulárním model checkingem, což je technika pro analýzu programů, jejíchž stavový prostor může být nekonečný v důsledku práce například s neomezenými frontami, parametry, dynamicky propojenými datovými strukturami, rekurzivními procedurami nebo řetězci. Cílem této práce bylo implementovat vylepšení stávajícího prototypu nástroje ASMA implementujícího regulárním model checking nad knihovnou Automata of Microsoftu. Provedli jsme analýzu zdrojového kódu nástroje ASMA a zopakovaly analýzy všech dostupných srovnávacích programů. Identifikovali jsme některá úzká místa a několik z nich jsme vyřešili. Zejména jsme integrovali knihovnu obsahující další redukční algoritmy do nástroje ASMA, vytvořili několik nových verzí operace reverzní konkatenace, která se v benchmarcích ukázala jako velmi nákladná, vylepšili rozhraní příkazového řádku ASMA a implementovali některé další optimalizace. Výpočetní čas se při analýze větších programů snížil o 90 %.
|
|
|
Measurement of the magnetic properties of materials using LabVIEW
Šolc, Martin ; Bulín, Tomáš (referee) ; Huzlík, Rostislav (advisor)
In this thesis LabVIEW program and its development environment is described. After that the most used current transducers, their working principles and their properties are analyzed. Next part is dedicated to curves of magnetic hysteresis of ferromagnetic materials. Practical part of bachelor´s thesis is dedicated to measuring BH curves of torroidal core transformer. The measuring was made possible by LabVIEW program, using digital integration in LabVIEW, analog integration with RC cell, voltage converter and current transducer ITN 12-P Ultrastab. In the last part of the bachelor´s thesis I evaluate the measurements.
|
|
|
Data Acquisition and Control System of Hydroelectric Power Plant Using Internet Techniques
Sattouf, Mousa ; Přikryl, Hynek (referee) ; Richter, Aleš (referee) ; Skalický, Jiří (advisor)
Vodní energie se nyní stala nejlepším zdrojem elektrické energie na zemi. Vyrábí se pomocí energie poskytované pohybem nebo pádem vody. Historie dokazuje, že náklady na tuto elektrickou energii zůstávají konstantní v průběhu celého roku. Vzhledem k mnoha výhodám, většina zemí nyní využívá vodní energie jako hlavní zdroj pro výrobu elektrické energie.Nejdůležitější výhodou je, že vodní energie je zelená energie, což znamená, že žádné vzdušné nebo vodní znečišťující látky nejsou vyráběny, také žádné skleníkové plyny jako oxid uhličitý nejsou vyráběny, což činí tento zdroj energie šetrný k životnímu prostředí. A tak brání nebezpečí globálního oteplování. Použití internetové techniky k ovladání několika vodních elektráren má velmi významné výhody, jako snížení provozních nákladů a flexibilitu uspokojení změny poptávky po energii na straně spotřeby. Také velmi efektivně čelí velkým narušením elektrické sítě, jako je například přidání nebo odebrání velké zátěže, a poruch. Na druhou stranu, systém získávání dat poskytuje velmi užitečné informace pro typické i vědecké analýzy, jako jsou ekonomické náklady, predikce poruchy systémů, predikce poptávky, plány údržby, systémů pro podporu rozhodování a mnoho dalších výhod. Tato práce popisuje všeobecný model, který může být použit k simulaci pro sběr dat a kontrolní systémy pro vodní elektrárny v prostředí Matlab / Simulink a TrueTime Simulink knihovnu. Uvažovaná elektrárna sestává z vodní turbíny připojené k synchronnímu generátoru s budicí soustavou, generátor je připojen k veřejné elektrické síti. Simulací vodní turbíny a synchronního generátoru lze provést pomocí různých simulačních nástrojů. V této práci je upřednostňován SIMULINK / MATLAB před jinými nástroji k modelování dynamik vodní turbíny a synchronního stroje. Program s prostředím MATLAB SIMULINK využívá k řešení schematický model vodní elektrárny sestavený ze základních funkčních bloků. Tento přístup je pedagogicky lepší než komplikované kódy jiných softwarových programů. Knihovna programu Simulink obsahuje funkční bloky, které mohou být spojovány, upravovány a modelovány. K vytvoření a simulování internetových a Real Time systémů je možné použít bud‘ knihovnu simulinku Real-Time nebo TRUETIME, v práci byla použita knihovna TRUETIME.
|
|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
V této práci se zabýváme regulárním model checkingem, což je technika pro analýzu programů, jejíchž stavový prostor může být nekonečný v důsledku práce například s neomezenými frontami, parametry, dynamicky propojenými datovými strukturami, rekurzivními procedurami nebo řetězci. Cílem této práce bylo implementovat vylepšení stávajícího prototypu nástroje ASMA implementujícího regulárním model checking nad knihovnou Automata of Microsoftu. Provedli jsme analýzu zdrojového kódu nástroje ASMA a zopakovaly analýzy všech dostupných srovnávacích programů. Identifikovali jsme některá úzká místa a několik z nich jsme vyřešili. Zejména jsme integrovali knihovnu obsahující další redukční algoritmy do nástroje ASMA, vytvořili několik nových verzí operace reverzní konkatenace, která se v benchmarcích ukázala jako velmi nákladná, vylepšili rozhraní příkazového řádku ASMA a implementovali některé další optimalizace. Výpočetní čas se při analýze větších programů snížil o 90 %.
|
|
|
Tool for Abstract Regular Model Checking
Chalk, Matěj ; Rogalewicz, Adam (referee) ; Hruška, Martin (advisor)
Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.
|
guest ::
